Inference at * 1 0 
Iof proof for Lemma equiv rel iff:



  Refl(;A,B.A  B) & Sym(;A,B.A  B) & Trans(;A,B.A  B) 

latex

 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{3:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{13:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{9:n,
 by PERMUTE{3:n} 

latex

 1: 

 1: 1. a : 
 1: 2. a
 1:   a
 2: .....wf..... NILNIL

 2: 1. a : 
 2:   a  
 3: .....wf..... NILNIL

 3:     Type
 4: 

 4: 1. a : 
 4: 2. b : 
 4: 3. a  b
 4: 4. b
 4:   a
 5: .....wf..... NILNIL

 5: 1. a : 
 5: 2. b : 
 5: 3. a  b
 5:   b  
 6: 

 6: 1. a : 
 6: 2. b : 
 6: 3. a  b
 6: 4. a
 6:   b
 7: .....wf..... NILNIL

 7: 1. a : 
 7: 2. b : 
 7: 3. a  b
 7:   a  
 8: .....wf..... NILNIL

 8: 1. a : 
 8: 2. b : 
 8:   (a  b)  
 9: .....wf..... NILNIL

 9: 1. 
 9:     Type
 10: 

 10: 1. a : 
 10: 2. b : 
 10: 3. c : 
 10: 4. a  b
 10: 5. b  c
 10: 6. a
 10:   c
 11: .....wf..... NILNIL

 11: 1. a : 
 11: 2. b : 
 11: 3. c : 
 11: 4. a  b
 11: 5. b  c
 11:   a  
 12: 

 12: 1. a : 
 12: 2. b : 
 12: 3. c : 
 12: 4. a  b
 12: 5. b  c
 12: 6. c
 12:   a
 13: .....wf..... NILNIL

 13: 1. a : 
 13: 2. b : 
 13: 3. c : 
 13: 4. a  b
 13: 5. b  c
 13:   c  
 14: .....wf..... NILNIL

 14: 1. a : 
 14: 2. b : 
 14: 3. c : 
 14: 4. a  b
 14:   (b  c)  
 15: .....wf..... NILNIL

 15: 1. a : 
 15: 2. b : 
 15: 3. 
 15:   (a  b)  
 16: .....wf..... NILNIL

 16: 1. 
 16: 2. 
 16:     Type
 .

Definitions

t  T, Type, s = t, x:AB(x), x:A  B(x), , P  Q, P  Q, x:A. B(x), Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), P  Q, Refl(T;x,y.E(x;y)), P & Q